/-
Copyright (c) 2020 David Wärn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Wärn
-/
import logic.encodable.basic
import order.atoms
import order.upper_lower.basic

/-!
# Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

## Main definitions

Throughout this file, `P` is at least a preorder, but some sections require more
structure, such as a bottom element, a top element, or a join-semilattice structure.
- `order.ideal P`: the type of nonempty, upward directed, and downward closed subsets of `P`.
  Dual to the notion of a filter on a preorder.
- `order.is_ideal P`: a predicate for when a `set P` is an ideal.
- `order.ideal.principal p`: the principal ideal generated by `p : P`.
- `order.ideal.is_proper P`: a predicate for proper ideals.
  Dual to the notion of a proper filter.
- `order.ideal.is_maximal`: a predicate for maximal ideals.
  Dual to the notion of an ultrafilter.
- `order.cofinal P`: the type of subsets of `P` containing arbitrarily large elements.
  Dual to the notion of 'dense set' used in forcing.
- `order.ideal_of_cofinals p 𝒟`, where `p : P`, and `𝒟` is a countable family of cofinal
  subsets of P: an ideal in `P` which contains `p` and intersects every set in `𝒟`. (This a form
  of the Rasiowa–Sikorski lemma.)

## References

- <https://en.wikipedia.org/wiki/Ideal_(order_theory)>
- <https://en.wikipedia.org/wiki/Cofinal_(mathematics)>
- <https://en.wikipedia.org/wiki/Rasiowa%E2%80%93Sikorski_lemma>

Note that for the Rasiowa–Sikorski lemma, Wikipedia uses the opposite ordering on `P`,
in line with most presentations of forcing.

## Tags

ideal, cofinal, dense, countable, generic

-/

open function set

namespace order

variables {P : Type*}

/-- An ideal on an order `P` is a subset of `P` that is
  - nonempty
  - upward directed (any pair of elements in the ideal has an upper bound in the ideal)
  - downward closed (any element less than an element of the ideal is in the ideal). -/
structure ideal (P) [has_le P] extends lower_set P :=
(nonempty'  : carrier.nonempty)
(directed'  : directed_on (≤) carrier)

/-- A subset of a preorder `P` is an ideal if it is
  - nonempty
  - upward directed (any pair of elements in the ideal has an upper bound in the ideal)
  - downward closed (any element less than an element of the ideal is in the ideal). -/
@[mk_iff] structure is_ideal {P} [has_le P] (I : set P) : Prop :=
(is_lower_set : is_lower_set I)
(nonempty : I.nonempty)
(directed : directed_on (≤) I)

/-- Create an element of type `order.ideal` from a set satisfying the predicate
`order.is_ideal`. -/
def is_ideal.to_ideal [has_le P] {I : set P} (h : is_ideal I) : ideal P :=
⟨⟨I, h.is_lower_set⟩, h.nonempty, h.directed⟩

namespace ideal
section has_le
variables [has_le P]

section
variables {I J s t : ideal P} {x y : P}

lemma to_lower_set_injective : injective (to_lower_set : ideal P → lower_set P) :=
λ s t h, by { cases s, cases t, congr' }

instance : set_like (ideal P) P :=
{ coe := λ s, s.carrier,
  coe_injective' := λ s t h, to_lower_set_injective $ set_like.coe_injective h }

@[ext] lemma ext {s t : ideal P} : (s : set P) = t → s = t := set_like.ext'

@[simp] lemma carrier_eq_coe (s : ideal P) : s.carrier = s := rfl
@[simp] lemma coe_to_lower_set (s : ideal P) : (s.to_lower_set : set P) = s := rfl

protected lemma lower (s : ideal P) : is_lower_set (s : set P) := s.lower'
protected lemma nonempty (s : ideal P) : (s : set P).nonempty := s.nonempty'
protected lemma directed (s : ideal P) : directed_on (≤) (s : set P) := s.directed'
protected lemma is_ideal (s : ideal P) : is_ideal (s : set P) := ⟨s.lower, s.nonempty, s.directed⟩

lemma mem_compl_of_ge {x y : P} : x ≤ y → x ∈ (I : set P)ᶜ → y ∈ (I : set P)ᶜ := λ h, mt $ I.lower h

/-- The partial ordering by subset inclusion, inherited from `set P`. -/
instance : partial_order (ideal P) := partial_order.lift coe set_like.coe_injective

@[simp] lemma coe_subset_coe : (s : set P) ⊆ t ↔ s ≤ t := iff.rfl
@[simp] lemma coe_ssubset_coe : (s : set P) ⊂ t ↔ s < t := iff.rfl

@[trans] lemma mem_of_mem_of_le {x : P} {I J : ideal P} : x ∈ I → I ≤ J → x ∈ J :=
@set.mem_of_mem_of_subset P x I J

/-- A proper ideal is one that is not the whole set.
    Note that the whole set might not be an ideal. -/
@[mk_iff] class is_proper (I : ideal P) : Prop := (ne_univ : (I : set P) ≠ univ)

lemma is_proper_of_not_mem {I : ideal P} {p : P} (nmem : p ∉ I) : is_proper I :=
⟨λ hp, begin
  change p ∉ ↑I at nmem,
  rw hp at nmem,
  exact nmem (mem_univ p),
end⟩

/-- An ideal is maximal if it is maximal in the collection of proper ideals.

Note that `is_coatom` is less general because ideals only have a top element when `P` is directed
and nonempty. -/
@[mk_iff] class is_maximal (I : ideal P) extends is_proper I : Prop :=
(maximal_proper : ∀ ⦃J : ideal P⦄, I < J → (J : set P) = univ)

lemma inter_nonempty [is_directed P (≥)] (I J : ideal P) : (I ∩ J : set P).nonempty :=
begin
  obtain ⟨a, ha⟩ := I.nonempty,
  obtain ⟨b, hb⟩ := J.nonempty,
  obtain ⟨c, hac, hbc⟩ := exists_le_le a b,
  exact ⟨c, I.lower hac ha, J.lower hbc hb⟩,
end

end

section directed
variables [is_directed P (≤)] [nonempty P] {I : ideal P}

/-- In a directed and nonempty order, the top ideal of a is `univ`. -/
instance : order_top (ideal P) :=
{ top := ⟨⊤, univ_nonempty, directed_on_univ⟩,
  le_top := λ I, le_top }

@[simp] lemma top_to_lower_set : (⊤ : ideal P).to_lower_set = ⊤ := rfl
@[simp] lemma coe_top : ((⊤ : ideal P) : set P) = univ := rfl

lemma is_proper_of_ne_top (ne_top : I ≠ ⊤) : is_proper I := ⟨λ h, ne_top $ ext h⟩

lemma is_proper.ne_top (hI : is_proper I) : I ≠ ⊤ := λ h, is_proper.ne_univ $ congr_arg coe h

lemma _root_.is_coatom.is_proper (hI : is_coatom I) : is_proper I := is_proper_of_ne_top hI.1

lemma is_proper_iff_ne_top : is_proper I ↔ I ≠ ⊤ := ⟨λ h, h.ne_top, λ h, is_proper_of_ne_top h⟩

lemma is_maximal.is_coatom (h : is_maximal I) : is_coatom I :=
⟨is_maximal.to_is_proper.ne_top, λ J h, ext $ is_maximal.maximal_proper h⟩

lemma is_maximal.is_coatom' [is_maximal I] : is_coatom I := is_maximal.is_coatom ‹_›

lemma _root_.is_coatom.is_maximal (hI : is_coatom I) : is_maximal I :=
{ maximal_proper := λ _ _, by simp [hI.2 _ ‹_›],
  ..is_coatom.is_proper ‹_› }

lemma is_maximal_iff_is_coatom : is_maximal I ↔ is_coatom I := ⟨λ h, h.is_coatom, λ h, h.is_maximal⟩

end directed

section order_bot
variables [order_bot P]

@[simp] lemma bot_mem (s : ideal P) : ⊥ ∈ s := s.lower bot_le s.nonempty.some_mem

end order_bot

section order_top
variables [order_top P] {I : ideal P}

lemma top_of_top_mem (h : ⊤ ∈ I) : I = ⊤ := by { ext, exact iff_of_true (I.lower le_top h) trivial }

lemma is_proper.top_not_mem (hI : is_proper I) : ⊤ ∉ I := λ h, hI.ne_top $ top_of_top_mem h

end order_top
end has_le

section preorder
variables [preorder P]

section
variables {I J : ideal P} {x y : P}

/-- The smallest ideal containing a given element. -/
@[simps] def principal (p : P) : ideal P :=
{ to_lower_set := lower_set.Iic p,
  nonempty' := nonempty_Iic,
  directed' := λ x hx y hy, ⟨p, le_rfl, hx, hy⟩ }

instance [inhabited P] : inhabited (ideal P) := ⟨ideal.principal default⟩

@[simp] lemma principal_le_iff : principal x ≤ I ↔ x ∈ I :=
⟨λ h, h le_rfl, λ hx y hy, I.lower hy hx⟩

@[simp] lemma mem_principal : x ∈ principal y ↔ x ≤ y := iff.rfl

end

section order_bot
variables [order_bot P]

/-- There is a bottom ideal when `P` has a bottom element. -/
instance : order_bot (ideal P) :=
{ bot := principal ⊥,
  bot_le := by simp }

@[simp] lemma principal_bot : principal (⊥ : P) = ⊥ := rfl

end order_bot

section order_top
variables [order_top P]

@[simp] lemma principal_top : principal (⊤ : P) = ⊤ := to_lower_set_injective $ lower_set.Iic_top

end order_top
end preorder

section semilattice_sup
variables [semilattice_sup P] {x y : P} {I s : ideal P}

/-- A specific witness of `I.directed` when `P` has joins. -/
lemma sup_mem (hx : x ∈ s) (hy : y ∈ s) : x ⊔ y ∈ s :=
let ⟨z, hz, hx, hy⟩ := s.directed x hx y hy in s.lower (sup_le hx hy) hz

@[simp] lemma sup_mem_iff : x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I :=
⟨λ h, ⟨I.lower le_sup_left h, I.lower le_sup_right h⟩, λ h, sup_mem h.1 h.2⟩

end semilattice_sup

section semilattice_sup_directed
variables [semilattice_sup P] [is_directed P (≥)] {x : P} {I J K s t : ideal P}

/-- The infimum of two ideals of a co-directed order is their intersection. -/
instance : has_inf (ideal P) :=
⟨λ I J, { to_lower_set := I.to_lower_set ⊓ J.to_lower_set,
  nonempty' := inter_nonempty I J,
  directed' := λ x hx y hy, ⟨x ⊔ y, ⟨sup_mem hx.1 hy.1, sup_mem hx.2 hy.2⟩, by simp⟩ }⟩

/-- The supremum of two ideals of a co-directed order is the union of the down sets of the pointwise
supremum of `I` and `J`. -/
instance : has_sup (ideal P) :=
⟨λ I J, { carrier   := {x | ∃ (i ∈ I) (j ∈ J), x ≤ i ⊔ j},
  nonempty' := by { cases inter_nonempty I J, exact ⟨w, w, h.1, w, h.2, le_sup_left⟩ },
  directed' := λ x ⟨xi, _, xj, _, _⟩ y ⟨yi, _, yj, _, _⟩,
    ⟨x ⊔ y,
     ⟨xi ⊔ yi, sup_mem ‹_› ‹_›,
      xj ⊔ yj, sup_mem ‹_› ‹_›,
      sup_le
        (calc x ≤ xi ⊔ xj               : ‹_›
         ...    ≤ (xi ⊔ yi) ⊔ (xj ⊔ yj) : sup_le_sup le_sup_left le_sup_left)
        (calc y ≤ yi ⊔ yj               : ‹_›
         ...    ≤ (xi ⊔ yi) ⊔ (xj ⊔ yj) : sup_le_sup le_sup_right le_sup_right)⟩,
     le_sup_left, le_sup_right⟩,
  lower' := λ x y h ⟨yi, _, yj, _, _⟩, ⟨yi, ‹_›, yj, ‹_›, h.trans ‹_›⟩ }⟩

instance : lattice (ideal P) :=
{ sup          := (⊔),
  le_sup_left  := λ I J (i ∈ I), by { cases J.nonempty, exact ⟨i, ‹_›, w, ‹_›, le_sup_left⟩ },
  le_sup_right := λ I J (j ∈ J), by { cases I.nonempty, exact ⟨w, ‹_›, j, ‹_›, le_sup_right⟩ },
  sup_le       := λ I J K hIK hJK a ⟨i, hi, j, hj, ha⟩,
    K.lower ha $ sup_mem (mem_of_mem_of_le hi hIK) (mem_of_mem_of_le hj hJK),
  inf          := (⊓),
  inf_le_left  := λ I J, inter_subset_left I J,
  inf_le_right := λ I J, inter_subset_right I J,
  le_inf       := λ I J K, subset_inter,
  .. ideal.partial_order }

@[simp] lemma coe_sup : ↑(s ⊔ t) = {x | ∃ (a ∈ s) (b ∈ t), x ≤ a ⊔ b} := rfl
@[simp] lemma coe_inf : (↑(s ⊓ t) : set P) = s ∩ t := rfl
@[simp] lemma mem_inf : x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J := iff.rfl
@[simp] lemma mem_sup : x ∈ I ⊔ J ↔ ∃ (i ∈ I) (j ∈ J), x ≤ i ⊔ j := iff.rfl

lemma lt_sup_principal_of_not_mem (hx : x ∉ I) : I < I ⊔ principal x :=
le_sup_left.lt_of_ne $ λ h, hx $ by simpa only [left_eq_sup, principal_le_iff] using h

end semilattice_sup_directed

section semilattice_sup_order_bot
variables [semilattice_sup P] [order_bot P] {x : P} {I J K : ideal P}

instance : has_Inf (ideal P) :=
⟨λ S, { to_lower_set := ⨅ s ∈ S, to_lower_set s,
  nonempty' := ⟨⊥, begin
    rw [lower_set.carrier_eq_coe, lower_set.coe_infi₂, set.mem_Inter₂],
    exact λ s _, s.bot_mem,
  end⟩,
  directed' := λ a ha b hb, ⟨a ⊔ b, ⟨
    begin
      rw [lower_set.carrier_eq_coe, lower_set.coe_infi₂, set.mem_Inter₂] at ⊢ ha hb,
      exact λ s hs, sup_mem (ha _ hs) (hb _ hs),
    end,
    le_sup_left, le_sup_right⟩⟩ }⟩

variables {S : set (ideal P)}

@[simp] lemma coe_Inf : (↑(Inf S) : set P) = ⋂ s ∈ S, ↑s := lower_set.coe_infi₂ _

@[simp] lemma mem_Inf : x ∈ Inf S ↔ ∀ s ∈ S, x ∈ s :=
by simp_rw [←set_like.mem_coe, coe_Inf, mem_Inter₂]

instance : complete_lattice (ideal P) :=
{ ..ideal.lattice,
  ..complete_lattice_of_Inf (ideal P) (λ S, begin
    refine ⟨λ s hs, _, λ s hs, by rwa [←coe_subset_coe, coe_Inf, subset_Inter₂_iff]⟩,
    rw [←coe_subset_coe, coe_Inf],
    exact bInter_subset_of_mem hs,
  end) }

end semilattice_sup_order_bot

section distrib_lattice

variables [distrib_lattice P]
variables {I J : ideal P}

lemma eq_sup_of_le_sup {x i j: P} (hi : i ∈ I) (hj : j ∈ J) (hx : x ≤ i ⊔ j) :
  ∃ (i' ∈ I) (j' ∈ J), x = i' ⊔ j' :=
begin
  refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, _⟩,
  calc
  x    = x ⊓ (i ⊔ j)       : left_eq_inf.mpr hx
  ...  = (x ⊓ i) ⊔ (x ⊓ j) : inf_sup_left,
end

lemma coe_sup_eq : ↑(I ⊔ J) = {x | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j} :=
set.ext $ λ _, ⟨λ ⟨_, _, _, _, _⟩, eq_sup_of_le_sup ‹_› ‹_› ‹_›,
  λ ⟨i, _, j, _, _⟩, ⟨i, ‹_›, j, ‹_›, le_of_eq ‹_›⟩⟩

end distrib_lattice

section boolean_algebra

variables [boolean_algebra P] {x : P} {I : ideal P}

lemma is_proper.not_mem_of_compl_mem (hI : is_proper I) (hxc : xᶜ ∈ I) : x ∉ I :=
begin
  intro hx,
  apply hI.top_not_mem,
  have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›,
  rwa sup_compl_eq_top at ht,
end

lemma is_proper.not_mem_or_compl_not_mem (hI : is_proper I) : x ∉ I ∨ xᶜ ∉ I :=
have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem, by tauto

end boolean_algebra

end ideal

/-- For a preorder `P`, `cofinal P` is the type of subsets of `P`
  containing arbitrarily large elements. They are the dense sets in
  the topology whose open sets are terminal segments. -/
structure cofinal (P) [preorder P] :=
(carrier : set P)
(mem_gt  : ∀ x : P, ∃ y ∈ carrier, x ≤ y)

namespace cofinal

variables [preorder P]

instance : inhabited (cofinal P) :=
⟨{ carrier := univ, mem_gt := λ x, ⟨x, trivial, le_rfl⟩ }⟩

instance : has_mem P (cofinal P) := ⟨λ x D, x ∈ D.carrier⟩

variables (D : cofinal P) (x : P)
/-- A (noncomputable) element of a cofinal set lying above a given element. -/
noncomputable def above : P := classical.some $ D.mem_gt x

lemma above_mem : D.above x ∈ D :=
exists.elim (classical.some_spec $ D.mem_gt x) $ λ a _, a

lemma le_above : x ≤ D.above x :=
exists.elim (classical.some_spec $ D.mem_gt x) $ λ _ b, b

end cofinal

section ideal_of_cofinals

variables [preorder P] (p : P) {ι : Type*} [encodable ι] (𝒟 : ι → cofinal P)

/-- Given a starting point, and a countable family of cofinal sets,
  this is an increasing sequence that intersects each cofinal set. -/
noncomputable def sequence_of_cofinals : ℕ → P
| 0 := p
| (n+1) := match encodable.decode ι n with
           | none   := sequence_of_cofinals n
           | some i := (𝒟 i).above (sequence_of_cofinals n)
           end

lemma sequence_of_cofinals.monotone : monotone (sequence_of_cofinals p 𝒟) :=
by { apply monotone_nat_of_le_succ, intros n, dunfold sequence_of_cofinals,
  cases encodable.decode ι n, { refl }, { apply cofinal.le_above }, }

lemma sequence_of_cofinals.encode_mem (i : ι) :
  sequence_of_cofinals p 𝒟 (encodable.encode i + 1) ∈ 𝒟 i :=
by { dunfold sequence_of_cofinals, rw encodable.encodek, apply cofinal.above_mem, }

/-- Given an element `p : P` and a family `𝒟` of cofinal subsets of a preorder `P`,
  indexed by a countable type, `ideal_of_cofinals p 𝒟` is an ideal in `P` which
  - contains `p`, according to `mem_ideal_of_cofinals p 𝒟`, and
  - intersects every set in `𝒟`, according to `cofinal_meets_ideal_of_cofinals p 𝒟`.

  This proves the Rasiowa–Sikorski lemma. -/
def ideal_of_cofinals : ideal P :=
{ carrier   := { x : P | ∃ n, x ≤ sequence_of_cofinals p 𝒟 n },
  lower'     := λ x y hxy ⟨n, hn⟩, ⟨n, le_trans hxy hn⟩,
  nonempty' := ⟨p, 0, le_rfl⟩,
  directed' := λ x ⟨n, hn⟩ y ⟨m, hm⟩,
               ⟨_, ⟨max n m, le_rfl⟩,
               le_trans hn $ sequence_of_cofinals.monotone p 𝒟 (le_max_left _ _),
               le_trans hm $ sequence_of_cofinals.monotone p 𝒟 (le_max_right _ _) ⟩ }

lemma mem_ideal_of_cofinals : p ∈ ideal_of_cofinals p 𝒟 := ⟨0, le_rfl⟩

/-- `ideal_of_cofinals p 𝒟` is `𝒟`-generic. -/
lemma cofinal_meets_ideal_of_cofinals (i : ι) : ∃ x : P, x ∈ 𝒟 i ∧ x ∈ ideal_of_cofinals p 𝒟 :=
⟨_, sequence_of_cofinals.encode_mem p 𝒟 i, _, le_rfl⟩

end ideal_of_cofinals

end order
